FDL - Step of Proof: bool-to-neg-dcdr_wf

Step of Proof: bool-to-neg-dcdr_wf

Inference at * 1
Iof proof for Lemma bool-to-neg-dcdr wf:

1. A : Type
2. f : A

3. x : A

{f}

(x)

Dec(f(x) = ff)

by Assert {f}

(

x:A. Dec(f(x) = ff))

1: .....assertion..... NILNIL

1:

{f}

(

x:A. Dec(f(x) = ff))

2:

2: 4. {f}

(

x:A. Dec(f(x) = ff))

2:

{f}

(x)

Dec(f(x) = ff)

.

Definitions t T, x:A. B(x), Dec(P), s = t, , f(a), ff, {f}